g:OGrp, a, b, c:|g|. (a < b)  ((c * a) < (c * b)) 

latex

Up	groups 1
Definitions of Statement	IMonoid, Mon, AbMon, IGroup, OCMon, OGrp
Definitions	t  T, P  Q, P  Q, P & Q, x f y, P  Q, x:A. B(x), IMonoid, IGroup, True, T, , Mon, AbMon, OCMon, OGrp
Lemmas	ocgrp wf, grp car wf, grp op wf, grp lt wf, grp op preserves lt, grp inv wf, inverse wf, grp id wf, monoid p wf, grp inv assoc, grp sig wf, true wf, squash wf